\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$), $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, $n$:$\mathbb{N}$,\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it da}$(rcv($l$,${\it tg}$))?!Void()), ${\it es}$:ES.
\-\\[0ex](source($l$) = $i$)
\\[0ex]$\Rightarrow$ es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ \=(@$i$[[$A$;$k$ sends on $l$ with tag ${\it tg}$ [$s$,$v$.$f$($s$,$v$)], at marker $n$]]\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;${\it da}$(rcv($l$,${\it tg}$))?Top;${\it ds}$;$e$.kind($e$) = $k$\+
\\[0ex]\& ecl{-}es{-}act(${\it es}$;$n$;$A$)(es{-}init(${\it es}$;$e$),$e$);$e$.$f$((state when $e$),val($e$))))
\-\-
\end{tabbing}